#ifndef __CLAUSE_H__
#define __CLAUSE_H__

#include "memory.h"
#include "literal.h"

// Borrowed from MiniSat 1.14. Modified for CUDA device only.
//=================================================================================================
// Clause -- a simple class for representing a clause:

class Clause {
public:
    // NOTE: DO NOT use this constructor directly (doesn't allocate enough memory).
	__host__ __device__
	explicit Clause( int index, bool learnt, Lit* litArr, int beginId, int endId )
	: _size(endId - beginId), _learnt(learnt), _remove(false), _index(index), _hash(0)
	{
		for ( int i = beginId, j = 0; i < endId; ++i, ++j )
		{
			_data[j] = litArr[i];
			_hash += litArr[i].hash();
		}
#ifdef DEBUG_CUDASAT
		printf("[Clause] _index = %d, _size = %d, _hash = %d\n", _index, _size, _hash );
#endif
	}

	__host__ __device__
	~Clause() {}

    // -- use this function instead:
	friend Clause* Clause_new( int index, bool learnt, Lit* litArr, int beginId, int endId );

	__host__ __device__
	int size() const { return _size; }
    __host__ __device__
	bool get_learnt() const	{ return _learnt; }
    __host__ __device__
	bool get_remove() const	{ return _remove; }
    __host__ __device__
	void set_remove() { _remove = true; }
    __host__ __device__
	unsigned int get_hash() const { return _hash; }
    __host__ __device__
	int index() { return _index; }
    __host__ __device__
	void set_index( int index ) { _index = index; }
    __host__ __device__
	void erase( int index )
	{
#ifdef ASSERT
		if ( (index < 0) || (index >= _size) )
		{ printf( "[Clause] Assertion failed: erase() index = %d out of range.\n", index ); }
#endif
		--_size;
		for ( int i = index; i < _size; ++i )
		{ _data[i] = _data[i+1]; }
	}
    __host__ __device__
	Lit data ( int i ) const { return _data[i]; }
    __host__ __device__
	Lit* data_pointer ( int i ) { return &_data[i]; }

private:
	int				_size;
	bool			_learnt;
	bool			_remove;
	int				_index;
	unsigned int	_hash;
    Lit				_data[2]; // This doesn't allocate enough memory.
};

// Use this to create a new clause.
__host__ __device__ inline
Clause* Clause_new( int index, bool learnt, Lit* litArr, int beginId, int endId )
{
	if ( (endId - beginId) < 0 )
	{ printf( "[Clause] Error: (endId - beginId) < 0\n" ); }

	void* mem = xmalloc<char>( sizeof(Clause) - (sizeof(Lit) * 2) + (sizeof(Lit) * (endId - beginId)) );
    return new (mem) Clause( index, learnt, litArr, beginId, endId );
}

#endif /* __CLAUSE_H__ */
